3.4.1.3 Grammar Rules

3.4.1.3 Grammar Rules

PCSP System is based on CSP Module extended with probability syntax as highlighted below. Other syntax can be found in CSP Grammar Rules.

assertion

: '#' 'assert' definitionRef

(

( '|=' ( '(' | ')' | '[]' | '<>' | (ID - 'X') | STRING | '!' | '?' | '&&' | '||' | '->' | '<->' | '/\\' | '\\/' | '.' | INT )+ withClause)

| 'deadlockfree' withClause

| 'nonterminating' withClause

| 'deterministic'

| 'reaches' ID withClauseReach

| 'refines' definitionRef withClause

| 'refines' '<F>' definitionRef

| 'refines' '<FD>' definitionRef

| 'refines' '<T>' definitionRef

)

';'

;

withClause
: 'with' ('pmax' | 'pmin' | 'prob')

;

withClauseReach
: 'with' ('pmax' | 'pmin' | 'prob' | 'min' '(' expression ')' | 'max' '(' expression ')')

            ;
caseExpr
           : 'case'
              '{'   caseCondition+
                    ('default' ':' elsec=interleaveExpr)?
              '}'
            | 'pcase'
              '{'
                    pcaseCondition+
                    ('default' ':' elsec=interleaveExpr)?
              '}'
          | ifExpr
           ;

pcaseCondition
:'[' floatNumber ']' ':' interleaveExpr
;

floatNumber
: INT ('.' INT)?

;

timeoutExpr
: withinExpr ('timeout'^ '['! expression ']'! withinExpr)*
;

withinExpr
          : deadlineExpr
          | deadlineExpr 'within' '[' expression (',' expression)? ']'
          ;

deadlineExpr
: waituntilExpr 'deadline' '[' expression ']'

| waituntilExpr
;

waituntilExpr
: channelExpr 'waituntil' '[' expression ']'

| channelExpr
;